COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	10-24
C00003 ENDMK
C⊗;
10-24
Should syntactic simplification be subsumed under macros?
Should it be part of an explicit metamathematical formulation?

10-28

10-02 The parts of Richard's procedure for making proofs in a
theory via a meta theory should be defined separately.